#pragma once

#include<cassert>
#include<cstdio>
#include<iostream>
#include<unordered_set>
#include<vector>
#include"graph.h"

using namespace std;

class components_computer
{
	int current_time_;
	vector<int> in_time_;
	vector<int> lowest_time_;
	vector<int> color_;
	vector<int> stack_;
	int current_component_;
	vector<int> component_;
public:
	void clear(const IGraph* graph);

	void on_stack(const IGraph* graph, int vertex_from, int vertex_to) {}
	void on_gray(const IGraph* graph, int vertex);
	void on_black(const IGraph* graph, int vertex);

	int component(int vertex) const
	{
		return component_[vertex];
	}
	int max_component() const
	{
		int max_component = 0;
		for (int vertex = 0; vertex < component_.size(); ++vertex)
			max_component = max(max_component, component_[vertex]);
		return max_component;
	}
};

void components_computer::clear(const IGraph* graph)
{
	current_time_ = 0;
	in_time_.resize(graph->get_vertices_number(), -1);
	lowest_time_.resize(graph->get_vertices_number(), graph->get_vertices_number());
	color_.resize(graph->get_vertices_number(), 0);
	stack_.clear();
	current_component_ = 0;
	component_.resize(graph->get_vertices_number(), -1);
}

void components_computer::on_gray(const IGraph* graph, int vertex)
{
	color_[vertex] = 1;
	stack_.push_back(vertex);
	in_time_[vertex] = current_time_;
	lowest_time_[vertex] = current_time_;
	++current_time_;
}

void components_computer::on_black(const IGraph* graph, int vertex)
{
	color_[vertex] = 2;
	vector<int> incidence = graph->get_incidence_list(vertex);
	for (int i = 0; i < incidence.size(); ++i)
		if (color_[incidence[i]] != 2 || component_[incidence[i]] < 0)
			lowest_time_[vertex] = min(lowest_time_[vertex], lowest_time_[incidence[i]]);
	if (in_time_[vertex] == lowest_time_[vertex])
	{
		while (stack_[stack_.size() - 1] != vertex)
		{
			component_[stack_[stack_.size() - 1]] = current_component_;
			stack_.pop_back();
		}
		component_[stack_[stack_.size() - 1]] = current_component_;
		stack_.pop_back();
		++current_component_;
	}
}

vector<int> get_strongly_connected_components(const IGraph* graph)
{
	int vertices_number = graph->get_vertices_number();
	components_computer f;
	dfs<components_computer>(graph, -1, &f);
	int max_component = f.max_component();
	vector<int> component;
	for (int vertex = 0; vertex < vertices_number; ++vertex)
		component.push_back(max_component - f.component(vertex));
	return component;
}

IGraph* condensate_graph(const IGraph* graph, const vector<int>& component)
{
	int vertices_number = graph->get_vertices_number();
	assert(vertices_number == component.size());
	int components_number = 0;
	for (int vertex = 0; vertex < vertices_number; ++vertex)
		components_number = max(components_number, component[vertex] + 1);
	vector<pair<int, int> > edges;
	unordered_set<int> is_edge;
	for (int vertex = 0; vertex < vertices_number; ++vertex)
	{
		vector<int> incidence = graph->get_incidence_list(vertex);
		for (int i = 0; i < incidence.size(); ++i)
		{
			int from = component[vertex], to = component[incidence[i]];
			if (from != to && (is_edge.insert(components_number * from + to)).second)
			{		
				pair<int, int> edge(from, to);	
				edges.push_back(edge);
			}
		}
	}
	IGraph* graph = make_compact_graph(components_number, edges);
	return graph;
}

int variable_to_vertex(int variable, int variables_number)
{
	if (variable > 0)
		return variable - 1;
	return -variable - 1 + variables_number;
}

IGraph* make_graph_from_expression(int variables_number, const vector<pair<int, int> >& disjuncts)
{
	vector<pair<int, int> > edges;
	for (int i = 0; i < disjuncts. size(); ++i)
	{
		int variable1 = disjuncts[i].first, variable2 = disjuncts[i].second;
		pair<int, int> implication_from_1_to_2(variable_to_vertex(-variable1, variables_number), variable_to_vertex(variable2, variables_number));
		edges.push_back(implication_from_1_to_2);
		pair<int, int> implication_from_2_to_1(variable_to_vertex(-variable2, variables_number), variable_to_vertex(variable1, variables_number));
		edges.push_back(implication_from_2_to_1);
	}
	IGraph* graph = make_compact_graph(2 * variables_number, edges);
	return graph;
}

bool has_solution(int variables_number, const vector<int>& component)
{
	for (int variable = 1; variable <= variables_number; ++variable)
		if (component[variable - 1] == component[variable - 1 + variables_number])
			return false;
	return true;
}

vector<int> get_solution(int variables_number, const vector<int>& component)
{
	vector<int> variable_value(variables_number + 1, -1); 
	for (int variable = 1; variable <= variables_number; ++variable)
		if (component[variable - 1] > component[variable - 1 + variables_number])
			variable_value[variable] = 1;
	return variable_value;
}

pair <bool, vector<int>> solve_2_sat(int variables_number, const vector<pair<int, int> >& disjuncts)
{
	IGraph* graph = make_graph_from_expression(variables_number, disjuncts);
	vector<int> component = get_strongly_connected_components(graph);
	delete graph;
	if (! has_solution(variables_number, component))
	{
		vector<int> empty;
		pair <bool, vector<int>> answer(false, empty);
		return answer;
	}
	pair <bool, vector<int>> answer(true, get_solution(variables_number, component));
	return answer;
}